\begin{tabbing} $\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl{-}trans{-}tuple\=\{i:l\}\+ \\[0ex](${\it ds}$; ${\it da}$). \-\\[0ex]ecl{-}trans{-}init($A$) $\in$ ecl{-}trans{-}type($A$) \end{tabbing}